Search Results: "adam"

10 June 2020

Evgeni Golov: show your desk

Some days ago I posted a picture of my desk on Mastodon and Twitter. standing desk with a monitor, laptop etc After that I got multiple questions about the setup, so I thought "Michael and Michael did posts about their setups, you could too!" And well, here we are ;-) desk The desk is a Flexispot E5B frame with a 200 80 2.6cm oak table top. The Flexispot E5 (the B stands for black) is a rather cheap (as in not expensive) standing desk frame. It has a retail price of 379 , but you can often get it as low as 299 on sale. Add a nice table top from a local store (mine was like 99 ), a bit of wood oil and work and you get a nice standing desk for less than 500 . The frame has three memory positions, but I only use two: one for sitting, one for standing, and a "change position" timer that I never used so far. The table top has a bit of a swing when in standing position (mine is at 104cm according to the electronics in the table), but not enough to disturb typing on the keyboard or thinking. I certainly wouldn't place a sewing machine up there, but that was not a requirement anyways ;) To compare: the IKEA Bekant table has a similar, maybe even slightly stronger swing. chair Speaking of IKEA The chair is an IKEA Volmar. They don't seem to sell it since mid 2019 anymore though, so no link here. hardware laptop A Lenovo ThinkPad T480s, i7-8650U, 24GB RAM, running Fedora 32 Workstation. Just enough power while not too big and heavy. Full of stickers, because I stickers! It's connected to a Lenovo ThinkPad Thunderbolt 3 Dock (Gen 1). After 2 years with that thing, I'm still not sure what to think about it, as I had various issues with it over the time:
  • the internal USB hub just vanishing from existence until a full power cycle of the dock was performed, but that might have been caused by my USB-switch which I recently removed.
  • the NIC negotiating at 100MBit/s instead of 1000MBit/s and then keeping on re-negotiating every few minutes, disconnecting me from the network, but I've not seen that since the Fedora 32 upgrade.
  • the USB-attached keyboard not working during boot as it needs some Thunderbolt magic.
The ThinkPad stands on a Adam Hall Stands SLT001E, a rather simple stand for laptops and other equipment (primarily made for DJs I think). The Dock fits exactly between the two feet of the stand, so that is nice and saves space on the table. Using the stand I can use the laptop screen as a second screen when I want it - but most often I do not and have the laptop lid closed while working. workstation A Lenovo ThinkStation P410, Xeon E5-2620 v4, 96GB RAM, running Fedora 32 Workstation. That's my VM playground. Having lots of RAM really helps if you need/want to run many VMs with Foreman/Katello or Red Hat Satellite as they tend to be a bit memory hungry and throwing hardware at problems tend to be an easy solution for many of them. The ThinkStation is also connected to the monitor, and I used to have an USB switch to flip my keyboard, mouse and Yubikey from the laptop to the workstation and back. But as noted above, this switch somehow made the USB hub in the laptop dock unhappy (maybe because I was switching too quickly after resume or so), so it's currently removed from the setup and I use the workstation via SSH only. It's mounted under the table using a ROLINE PC holder. You won't get any design awards with it, but it's easy to assemble and allows the computer to move with the table, minimizing the number of cables that need to have a flexible length. monitor The monitor is an older Dell UltraSharp U2515H - a 25" 2560 1440 model. It sits on an Amazon Basics Monitor Arm (which is identical to an Ergotron LX to the best of my knowledge) and is accompanied by a Dell AC511 soundbar. I don't use the adjustable arm much. It's from the time I had no real standing desk and would use the arm and a cardboard box to lift the monitor and keyboard to a standing level. If you don't want to invest in a standing desk, that's the best and cheapest solution! The soundbar is sufficient for listening to music while working and for chatting with colleagues. webcam A Logitech C920 Pro, what else? Works perfectly under Linux with the UVC driver and has rather good microphones. Actually, so good that I never use a headset during video calls and so far nobody complained about bad audio. keyboard A ThinkPad Compact USB Keyboard with TrackPoint. The keyboard matches the one in my T480s, so my brain doesn't have to switch. It was awful when I still had the "old" model and had to switch between the two. UK layout. Sue me. I like the big return key. mouse A Logitech MX Master 2. I got the MX Revolution as a gift a long time ago, and at first I was like: WTF, why would anyone pay hundred bucks for a mouse?! Well, after some time I knew, it's just that good. And when it was time to get a new one (the rubber coating gets all slippery after some time) the decision was rather easy. I'm pondering if I should try the MX Ergo or the MX Vertical at some point, but not enough to go and buy one of them yet. other notepad I'm terrible at remembering things, so I need to write them down. And I'm terrible at remembering to look at my notes, so they need to be in my view. So there is a regular A5 notepad on my desk, that gets filled with check boxes and stuff, page after page. coaster It's a wooden table, you don't want to have liquids on it, right? Thankfully a friend of mine once made coasters out of old Xeon CPUs and epoxy. He gave me one in exchange for a busted X41 ThinkPad. I still think I made the better deal ;) yubikey Keep your secrets safe! Mine is used as a GnuPG smart card for both encryption and SSH authentication, U2F on various pages and 2FA for VPN. headphones I own a pair of Bose QuietComfort 25 with an aftermarket Bluetooth adapter and Anker SoundBuds Slim+. Both are used rather seldomly while working, as my office is usually quiet and no one is disturbed when I listen to music without headphones. what's missing? light I want to add more light to the setup, noth to have a better picture during video calls but also to have better light when doing something else on the table - like soldering. The plan is to add an IKEA Tertial with some Tr dfri smart LED in it, but the Tertial is currently not available for delivery at IKEA and I'm not going to visit one in the current situation. bigger monitor Currently pondering getting a bigger (27+ inch) 4K monitor. Still can't really decide which one to get. There are so many, and they all differ in some way. But it seems no affordable one is offering an integrated USB switch and sufficient amount of USB ports, so I'll probably get whatever can get me a good picture without any extra features at a reasonable price. Changing the monitor will probably also mean rethinking the sound output, as I'm sure mounting the Dell soundbar to anything but the designated 5 year old monitor won't work too well.

3 June 2020

Keith Packard: picolibc-ryu

Float/String Conversion in Picolibc: Enter Ry I recently wrote about this topic having concluded that the best route for now was to use the malloc-free, but imprecise, conversion routines in the tinystdio alternative. A few days later, Sreepathi Pai pointed me at some very recent work in this area: This is amazing! Thirty years after the papers referenced in the previous post, Ulf Adams came up with some really cool ideas and managed to reduce the math required for 64-bit conversion to 128 bit integers. This is a huge leap forward; we were doing long multi-precision computations before, and now it's all short enough to fit in registers (ok, a lot of registers, but still). Getting the Ry Code The code is available on github: https://github.com/ulfjack/ryu. Reading through it, it's very clear that the author focuses on performance with lots of tuning for common cases. Still, it's quite readable, especially compared with the newlib multi-precision based code. Picolibc String/Float conversion interface Picolibc has some pretty basic needs for the float/string conversion code, it wants four functions:
  1. __dtoa_engine 
    int
__dtoa_engine(double x, struct dtoa *dtoa, uint8_t max_digits, uint8_t max_decimals);
    This converts the double x to a string of decimal digits and a decimal exponent stored inside the 'dtoa' struct. It limits the total number of digits to max_digits and, optionally (when max_decimals is non-zero), limits the number of fractional digits to max_decimals - 1. This latter supports 'f' formats. Returns the number of digits stored, which is <= max_digits. Less if the number can be accurately represented in fewer digits.
  2. __ftoa_engine 
    int
__ftoa_engine(float x, struct ftoa *ftoa, uint8_t max_digits, uint8_t max_decimals);
    The same as __dtoa_engine, except for floats.
  3. __atod_engine 
    double
__atod_engine(uint64_t m10, int e10);
    To avoid needing to handle stdio inside the conversion function, __atod_engine receives fully parsed values, the base-10 significand (m10) and exponent (e10). The value to convert is m10 * pow(10, e10).
  4. __atof_engine 
    float
__atof_engine(uint32_t m10, int e10);
    The same as __atod_engine, except for floats.
With these, it can do printf, scanf, ecvt, fcvt, gcvt, strtod, strtof and atof. Porting Ry to Picolibc The existing Ry float-to-string code always generates the number of digits necessary for accurate output. I had to hack it up to generate correctly rounded shorter output when max_digits or max_decimals were smaller. I'm not sure I managed to do that correctly, but at least it appears to be passing all of the test cases I have. In normal operation, Ry iteratively removes digits from the answer that aren't necessary to disambiguate with neighboring values. What I changed was to keep removing digits using that method until the answer had few enough digits to fit in the desired length. There's some tricky rounding code that adjusts the final result and I had to bypass that if I'd removed extra digits. That was about the only change necessary to the core algorithm. I also trimmed the code to only include the general case and not the performance improvements, then wrapped it with code to provide the _engine interface. On the string-to-float side, most of what I needed to do was remove the string parsing bits at the start of the function and switch from performance-optimized to space-optimized versions of a couple of internal routines. Correctness Results Because these new functions are now 'exact', I was able to adjust the picolibc tests to compare all of the bits for string/float conversion instead of having to permit a bit of slop in the answers. With those changes, the picolibc test suite passes, which offers some assurance that things aren't completely broken. Size Results Snek uses the 32-bit float versions of the conversion routines, and for that, the size difference is: 
   text    data     bss     dec     hex filename
  59068      44   37968   97080   17b38 snek-qemu-riscv-orig.elf
  59430      44   37968   97442   17ca2 snek-qemu-riscv-ryu.elf
    362
362 bytes added to gain accurate printf/strtof results seems like a good trade-off in this case. Performance I haven't measured performance at all, but I suspect that it won't be nearly as problematic on most platforms as the source code makes it appear. And that's because Ry is entirely integer arithmetic with no floating point at all. This avoids using the soft fp code for platforms without hardware float support. Pointers to the Code I haven't merged this to picolibc master yet, it's on the ryu branch: Review, especially of the hack above to return short results, would be greatly appreciated! Thanks again to Ulf Adams for creating this code and to Sreepathi Pai for sending me a note about it!

12 May 2020

Jacob Adams: Roman Finger Counting

I recently wrote a final paper on the history of written numerals. In the process, I discovered this fascinating tidbit that didn t really fit in my paper, but I wanted to put it somewhere. So I m writing about it here. If I were to ask you to count as high as you could on your fingers you d probably get up to 10 before running out of fingers. You can t count any higher than the number of fingers you have, right? The Romans could! They used a place-value system, combined with various gestures to count all the way up to 9,999 on two hands.

The System Finger Counting (Note that in this diagram 60 is, in fact, wrong, and this picture swaps the hundreds and the thousands.) We ll start with the units. The last three fingers of the left hand, middle, ring, and pinkie, are used to form them. Zero is formed with an open hand, the opposite of the finger counting we re used to. One is formed by bending the middle joint of the pinkie, two by including the ring finger and three by including the middle finger, all at the middle joint. You ll want to keep all these bends fairly loose, as otherwise these numbers can get quite uncomfortable. For four, you extend your pinkie again, for five, also raise your ring finger, and for six, you raise your middle finger as well, but then lower your ring finger. For seven you bend your pinkie at the bottom joint, for eight adding your ring finger, and for nine, including your middle finger. This mirrors what you did for one, two and three, but bending the finger at the bottom joint now instead. This leaves your thumb and index finger for the tens. For ten, touch the nail of your index finger to the inside of your top thumb joint. For twenty, put your thumb between your index and middle fingers. For thirty, touch the nails of your thumb and index fingers. For forty, bend your index finger slightly towards your palm and place your thumb between the middle and top knuckle of your index finger. For fifty, place your thumb against your palm. For sixty, leave your thumb where it is and wrap your index finger around it (the diagram above is wrong). For seventy, move your thumb so that the nail touches between the middle and top knuckle of your index finger. For eighty, flip your thumb so that the bottom of it now touches the spot between the middle and top knuckle of your index finger. For ninety, touch the nail of your index finger to your bottom thumb joint. The hundreds and thousands use the same positions on the right hand, with the units being the thousands and the tens being the hundreds. One account, from which the picture above comes, swaps these two, but the first account we have uses this ordering. Combining all these symbols, you can count all the way to 9,999 yourself on just two hands. Try it!

History

The Venerable Bede The first written record of this system comes from the Venerable Bede, an English Benedictine monk who died in 735. He wrote De computo vel loquela digitorum, On Calculating and Speaking with the Fingers, as the introduction to a larger work on chronology, De temporum ratione. (The primary calculation done by monks at the time was calculating the date of Easter, the first Sunday after the first full moon of spring). He also includes numbers from 10,000 to 1,000,000, but its unknown if these were inventions of the author and were likely rarely used regardless. They require moving your hands to various positions on your body, as illustrated below, from Jacob Leupold s Theatrum Arilhmetico-Geometricum, published in 1727: Finger Counting with Large Numbers

The Romans If Bede was the first to write it, how do we know that it came from Roman times? It s referenced in many Roman writings, including this bit from the Roman satirist Juvenal who died in 130:
Felix nimirum qui tot per saecula mortem distulit atque suos iam dextera computat annos. Happy is he who so many times over the years has cheated death And now reckons his age on the right hand.
Because of course the right hand is where one counts hundreds! There s also this Roman riddle:
Nunc mihi iam credas fieri quod posse negatur: octo tenes manibus, si me monstrante magistro sublatis septem reliqui tibi sex remanebunt. Now you shall believe what you would deny could be done: In your hands you hold eight, as my teacher once taught; Take away seven, and six still remain.
If you form eight with this system and then remove the symbol for seven, you get the symbol for six!

Sources My source for this blog post is Paul Broneer s 1969 English translation of Karl Menninger s Zahlwort und Ziffer (Number Words and Number Symbols).

1 May 2020

Utkarsh Gupta: FOSS Activites in April 2020

Here s my (seventh) monthly update about the activities I ve done in the F/L/OSS world.

Debian
It s been 14 months since I ve started contributing to Debian. And 4 months since I ve been a Debian Developer. And in this beautiful time, I had this opprotunity to do and learn lots of new and interesting things. And most importantly, meet and interact with lots of lovely people!
Debian is $home.

Uploads:

Other $things:
  • Attended Ruby team meeting. Logs here.
  • Attended Perl team LHF. Report here.
  • Sponsored a lot of uploads for William Desportes and Adam Cecile.
  • Mentoring for newcomers.
  • FTP Trainee reviewing.
  • Moderation of -project mailing list.
  • Applied for DUCI project for Google Summer of Code 2020.

Ruby2.7 Migration:
Ruby2.7 was recently released on 25th December, 2019. Santa s gift. Believe it or not. We, the Debian Ruby team, have been trying hard to make it migrate to testing. And it finally happened. The default version in testing is ruby2.7. Here s the news! \o/
Here s what I worked on this month for this transition.

Upstream: Opened several issues and proposed patches (in the form of PRs):
  • Issue #35 against encryptor for Ruby2.7 test failures.
  • Issue #28 against image_science for removing relative paths.
  • Issue #106 against ffi-yajl for Ruby2.7 test failures.
  • PR #5 against aggregate for simply using require.
  • PR #6 against aggregate for modernizing CI and adding Ruby 2.5 and 2.7 support.
  • Issue #13 against espeak-ruby for Ruby2.7 test failures.
  • Issue #4 against tty-which for test failures in general.
  • Issue #11 against packable for Ruby2.7 test failures. PR #12 has been proposed.
  • Issue #10 against growl for test failures and proposed an initial patch.

Downstream: I fixed and uploaded the following packages in Debian:

Debian LTS
Debian Long Term Support (LTS) is a project to extend the lifetime of all Debian stable releases to (at least) 5 years. Debian LTS is not handled by the Debian security team, but by a separate group of volunteers and companies interested in making it a success.
This was my seventh month as a Debian LTS paid contributor. I was assigned 24.00 hours and worked on the following things:

CVE Fixes and Announcements:

Other LTS Work:

Other(s)
Sometimes it gets hard to categorize work/things into a particular category.
That s why I am writing all of those things inside this category.
This includes two sub-categories and they are as follows.

Personal: This month I could get the following things done:
  • Most importantly, I finally migrated to a new website. Huge UI imporvement! \o/
    From Jekyll to Hugo, it was not easy. But it was worth it! Many thanks to Luiz for writing hugo-coder, Clement, and Samyak!
    If you find any flaws, issues and pull requests are welcomed at utkarsh2102/utkarsh2102.com
  • Wrote battery-alert, a mini-project of my own to show battery alerts at <10% and >90%.
    Written in shell, it brings me all the satisfaction as it has saved my life on many occasions.
    And guess what? It has more users than just myself!
    Reviews and patches are welcomed \o/
  • Mentored in HackOn Hackathon. Thanks to Manvi for reaching out!
    It was fun to see people developing some really nice projects.
  • Thanks to Ray and John, I became a GitLab Hero!
    (I am yet to figure out my role and responibility though)
  • Atteneded Intro Sec Con and had the most fun!
    Heard Ian s keynote and attended other talks and learned how to use WireShark!

Open Source: Again, this contains all the things that I couldn t categorize earlier.
Opened several issues and pull requests:
  • Issue #297 against hugo-coder, asking to enable RSS feed for blogs.
  • PR #316 for hugo-coder for fixing the above issue myself.
  • Issue #173 against arbre for requesting a release.
  • Issue #104 against combustion, asking to relax dependency on rubocop. Fixed in this commit.
  • Issue #16 against ffi-compiler for requesting to fix homepage and license.
  • Issue #57 against gographviz for requesting a release.
  • Issue #14 against crb-blast, suggesting compatability with bio 2.0.x.
  • Issue #58 against uniform_notifier for asking to drop the use of ruby-growl.
  • PR #2072 for polybar, adding installation instructions on Debian systems.
Until next time.
:wq for today.

15 April 2020

Antoine Beaupr : OpenDKIM configuration to send debian.org email

Debian.org added support for DKIM in 2020. To configure this on my side, I had to do the following, on top of my email configuration.
  1. add this line to /etc/opendkim/signing.table: 
    *@debian.org marcos-debian.anarcat.user
  2. add this line to /etc/opendkim/key.table: 
    marcos-debian.anarcat.user debian.org:marcos-debian.anarcat.user:/etc/opendkim/keys/marcos-debian.anarcat.user.private
    Yes, that's quite a mouthful! That magic selector is long in that way because it needs a special syntax (specifically the .anarcat.user suffix) for Debian to be happy. The -debian string is to tell me where the key is published. The marcos prefix is to remind me where the private is used.
  3. generate the key with: 
    opendkim-genkey --directory=/etc/opendkim/keys/ --selector=marcos-debian.anarcat.user --domain=debian.org --verbose
    This creates the DNS record in /etc/opendkim/keys/marcos-debian.anarcat.user.txt (alongside the private key in .key).
  4. restart OpenDKIM: 
    service opendkim restart
    The DNS record will look something like this: 
    marcos-debian.anarcat.user._domainkey   IN  TXT ( "v=DKIM1; h=sha256; k=rsa; "
"p=MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAtKzBK2f8vg5yV307WAOatOhypQt3ANQ95iDaewkVehmx42lZ6b4PzA1k5DkIarxjkk+7m6oSpx5H3egrUSLMirUiMGsIb5XVGBPFmKZhDVmC7F5G1SV7SRqqKZYrXTufRRSne1eEtA31xpMP0B32f6v6lkoIZwS07yQ7DDbwA9MHfyb6MkgAvDwNJ45H4cOcdlCt0AnTSVndcl"
"pci5/2o/oKD05J9hxFTtlEblrhDXWRQR7pmthN8qg4WaNI4WszbB3Or4eBCxhUdvAt2NF9c9eYLQGf0jfRsbOcjSfeus0e2fpsKW7JMvFzX8+O5pWfSpRpdPatOt80yy0eqpm1uQIDAQAB" )  ; ----- DKIM key marcos-debian.anarcat.user for debian.org
  5. The "p=MIIB..." string needs to be joined together, without the quotes and the p=, and sent in a signed email to changes@db.debian.org: 
    -----BEGIN PGP SIGNED MESSAGE-----
dkimPubKey: marcos.anarcat.user MIIB[...]
-----BEGIN PGP SIGNATURE-----
[...]
  6. Wait a few minutes for DNS to propagate. You can check if they have with: 
    host -t TXT marcos-debian.anarcat.user._domainkey.debian.org nsp.dnsnode.net
    (nsp.dnsnode.net being one of the NS records of the debian.org zone.)
If all goes well, the tests should pass when sending from your server as anarcat@debian.org.

Testing Test messages can be sent to dkimvalidator, mail-tester.com or check-auth@verifier.port25.com. Those tools will run Spamassassin on the received emails and report the results. What you are looking for is:
  • -0.1 DKIM_VALID: Message has at least one valid DKIM or DK signature
  • -0.1 DKIM_VALID_AU: Message has a valid DKIM or DK signature from author's domain
  • -0.1 DKIM_VALID_EF: Message has a valid DKIM or DK signature from envelope-from domain
If one of those is missing, then you are doing something wrong and your "spamminess" score will be worse. The latter is especially tricky as it validates the "Envelope From", which is the MAIL FROM: header as sent by the originating MTA, which you see as from=<> in the postfix lost. The following will happen anyways, as soon as you have a signature, that's normal:
  • 0.1 DKIM_SIGNED: Message has a DKIM or DK signature, not necessarily valid
And this might happen if you have a ADSP record but do not correctly sign the message with a domain field that matches the record:
  • 1.1 DKIM_ADSP_ALL No valid author signature, domain signs all mail
That's bad and will affect your spam core badly. I fixed that issue by using a wildcard key in the key table: 
--- a/opendkim/key.table
+++ b/opendkim/key.table
@@ -1 +1 @@
-marcos anarc.at:marcos:/etc/opendkim/keys/marcos.private
+marcos %:marcos:/etc/opendkim/keys/marcos.private

References This is a copy of a subset of my more complete email configuration.

22 March 2020

Enrico Zini: Notable people

Lotte Reiniger. The Unsung Heroine of Early Animation
history people wikipedia
2020-03-23
Lotte Reiniger pioneered early animation, yet her name remains largely unknown. We pay homage to her life and work, and reflect on why she never received the recognition she deserves.
Untangling the Tale of Ada Lovelace Stephen Wolfram Writings
history people archive.org
2020-03-23
Stephen Wolfram shares what he learned in researching Ada Lovelace's life, writings about the Analytical Engine, and computation of Bernoulli numbers.
Nellie Bly - Wikipedia
history people archive.org
2020-03-23
Elizabeth Cochran Seaman[1] (May 5, 1864[2] January 27, 1922), better known by her pen name Nellie Bly, was an American journalist who was widely known for her record-breaking trip around the world in 72 days, in emulation of Jules Verne's fictional character Phileas Fogg, and an expos in which she worked undercover to report on a mental institution from within.[3] She was a pioneer in her field, and launched a new kind of investigative journalism.[4] Bly was also a writer, inventor, and industrialist.
Delia Derbyshire - Wikipedia
history music people archive.org
2020-03-23
Delia Ann Derbyshire (5 May 1937 3 July 2001)[1] was an English musician and composer of electronic music.[2] She carried out pioneering work with the BBC Radiophonic Workshop during the 1960s, including her electronic arrangement of the theme music to the British science-fiction television series Doctor Who.[3][4] She has been referred to as "the unsung heroine of British electronic music,"[3] having influenced musicians including Aphex Twin, the Chemical Brothers and Paul Hartnoll of Orbital.[5]
Charity Adams Earley - Wikipedia
archive.org
2020-03-23
Charity Adams Earley (5 December 1918 13 January 2002) was the first African-American woman to be an officer in the Women's Army Auxiliary Corps (later WACS) and was the commanding officer of the first battalion of African-American women to serve overseas during World War II. Adams was the highest ranking African-American woman in the army by the completion of the war.

23 November 2017

Russ Allbery: Holiday haul

Catching up on accumulated book purchases. I'm going to get another burst of reading time over the holidays (and am really looking forward to it). Alfred Bester The Stars My Destination (sff)
James Blish A Case of Conscience (sff)
Leigh Brackett The Long Tomorrow (sff)
Algis Budrys Who? (sff)
Frances Hardinge Fly By Night (sff)
Robert A. Heinlein Double Star (sff)
N.K. Jemisin The Obelisk Gate (sff)
N.K. Jemisin The Stone Sky (sff)
T. Kingfisher Clockwork Boys (sff)
Ursula K. Le Guin City of Illusions (sff)
Ursula K. Le Guin The Complete Orsinia (historical)
Ursula K. Le Guin The Dispossessed (sff)
Ursula K. Le Guin Five Ways to Forgiveness (sff)
Ursula K. Le Guin The Left Hand of Darkness (sff)
Ursula K. Le Guin Planet of Exile (sff)
Ursula K. Le Guin Rocannon's World (sff)
Ursula K. Le Guin The Telling (sff)
Ursula K. Le Guin The World for Word Is Forest (sff)
Fritz Leiber The Big Time (sff)
Melina Marchetta Saving Francesca (mainstream)
Richard Matheson The Shrinking Man (sff)
Foz Meadows An Accident of Stars (sff)
Dexter Palmer Version Control (sff)
Frederick Pohl & C.M. Kornbluth The Space Merchants (sff)
Adam Rex True Meaning of Smekday (sff)
John Scalzi The Dispatcher (sff)
Julia Spencer-Fleming In the Bleak Midwinter (mystery)
R.E. Stearns Barbary Station (sff)
Theodore Sturgeon More Than Human (sff)
I'm listing the individual components except for the Orsinia collection, but the Le Guin are from the Library of America Hainish Novels & Stories two-volume set. I had several of these already, but I have a hard time resisting a high-quality Library of America collection for an author I really like. Now I can donate a bunch of old paperbacks. Similarly, a whole bunch of the older SF novels are from the Library of America American Science Fiction two-volume set, which I finally bought since I was ordering Library of America sets anyway. The rest is a pretty random collection of stuff, although several of them are recommendations from Light. I was reading through her old reviews and getting inspired to read (and review) more.

19 October 2017

Clint Adams: Scuttlebutt at the precinct

So who s getting patchwork into Debian?
Posted on 2017-10-19
Tags: bamamba

17 October 2017

Russ Allbery: Bundle haul

Confession time: I started making these posts (eons ago) because a close friend did as well, and I enjoyed reading them. But the main reason why I continue is because the primary way I have to keep track of the books I've bought and avoid duplicates is, well, grep on these posts. I should come up with a non-bullshit way of doing this, but time to do more elegant things is in short supply, and, well, it's my blog. So I'm boring all of you who read this in various places with my internal bookkeeping. I do try to at least add a bit of commentary. This one will be more tedious than most since it includes five separate Humble Bundles, which increases the volume a lot. (I just realized I'd forgotten to record those purchases from the past several months.) First, the individual books I bought directly: Ilona Andrews Sweep in Peace (sff)
Ilona Andrews One Fell Sweep (sff)
Steven Brust Vallista (sff)
Nicky Drayden The Prey of Gods (sff)
Meg Elison The Book of the Unnamed Midwife (sff)
Pat Green Night Moves (nonfiction)
Ann Leckie Provenance (sff)
Seanan McGuire Once Broken Faith (sff)
Seanan McGuire The Brightest Fell (sff)
K. Arsenault Rivera The Tiger's Daughter (sff)
Matthew Walker Why We Sleep (nonfiction)
Some new books by favorite authors, a few new releases I heard good things about, and two (Night Moves and Why We Sleep) from references in on-line articles that impressed me. The books from security bundles (this is mostly work reading, assuming I'll get to any of it), including a blockchain bundle: Wil Allsop Unauthorised Access (nonfiction)
Ross Anderson Security Engineering (nonfiction)
Chris Anley, et al. The Shellcoder's Handbook (nonfiction)
Conrad Barsky & Chris Wilmer Bitcoin for the Befuddled (nonfiction)
Imran Bashir Mastering Blockchain (nonfiction)
Richard Bejtlich The Practice of Network Security (nonfiction)
Kariappa Bheemaiah The Blockchain Alternative (nonfiction)
Violet Blue Smart Girl's Guide to Privacy (nonfiction)
Richard Caetano Learning Bitcoin (nonfiction)
Nick Cano Game Hacking (nonfiction)
Bruce Dang, et al. Practical Reverse Engineering (nonfiction)
Chris Dannen Introducing Ethereum and Solidity (nonfiction)
Daniel Drescher Blockchain Basics (nonfiction)
Chris Eagle The IDA Pro Book, 2nd Edition (nonfiction)
Nikolay Elenkov Android Security Internals (nonfiction)
Jon Erickson Hacking, 2nd Edition (nonfiction)
Pedro Franco Understanding Bitcoin (nonfiction)
Christopher Hadnagy Social Engineering (nonfiction)
Peter N.M. Hansteen The Book of PF (nonfiction)
Brian Kelly The Bitcoin Big Bang (nonfiction)
David Kennedy, et al. Metasploit (nonfiction)
Manul Laphroaig (ed.) PoC GTFO (nonfiction)
Michael Hale Ligh, et al. The Art of Memory Forensics (nonfiction)
Michael Hale Ligh, et al. Malware Analyst's Cookbook (nonfiction)
Michael W. Lucas Absolute OpenBSD, 2nd Edition (nonfiction)
Bruce Nikkel Practical Forensic Imaging (nonfiction)
Sean-Philip Oriyano CEHv9 (nonfiction)
Kevin D. Mitnick The Art of Deception (nonfiction)
Narayan Prusty Building Blockchain Projects (nonfiction)
Prypto Bitcoin for Dummies (nonfiction)
Chris Sanders Practical Packet Analysis, 3rd Edition (nonfiction)
Bruce Schneier Applied Cryptography (nonfiction)
Adam Shostack Threat Modeling (nonfiction)
Craig Smith The Car Hacker's Handbook (nonfiction)
Dafydd Stuttard & Marcus Pinto The Web Application Hacker's Handbook (nonfiction)
Albert Szmigielski Bitcoin Essentials (nonfiction)
David Thiel iOS Application Security (nonfiction)
Georgia Weidman Penetration Testing (nonfiction)
Finally, the two SF bundles: Buzz Aldrin & John Barnes Encounter with Tiber (sff)
Poul Anderson Orion Shall Rise (sff)
Greg Bear The Forge of God (sff)
Octavia E. Butler Dawn (sff)
William C. Dietz Steelheart (sff)
J.L. Doty A Choice of Treasons (sff)
Harlan Ellison The City on the Edge of Forever (sff)
Toh Enjoe Self-Reference ENGINE (sff)
David Feintuch Midshipman's Hope (sff)
Alan Dean Foster Icerigger (sff)
Alan Dean Foster Mission to Moulokin (sff)
Alan Dean Foster The Deluge Drivers (sff)
Taiyo Fujii Orbital Cloud (sff)
Hideo Furukawa Belka, Why Don't You Bark? (sff)
Haikasoru (ed.) Saiensu Fikushon 2016 (sff anthology)
Joe Haldeman All My Sins Remembered (sff)
Jyouji Hayashi The Ouroboros Wave (sff)
Sergei Lukyanenko The Genome (sff)
Chohei Kambayashi Good Luck, Yukikaze (sff)
Chohei Kambayashi Yukikaze (sff)
Sakyo Komatsu Virus (sff)
Miyuki Miyabe The Book of Heroes (sff)
Kazuki Sakuraba Red Girls (sff)
Robert Silverberg Across a Billion Years (sff)
Allen Steele Orbital Decay (sff)
Bruce Sterling Schismatrix Plus (sff)
Michael Swanwick Vacuum Flowers (sff)
Yoshiki Tanaka Legend of the Galactic Heroes, Volume 1: Dawn (sff)
Yoshiki Tanaka Legend of the Galactic Heroes, Volume 2: Ambition (sff)
Yoshiki Tanaka Legend of the Galactic Heroes, Volume 3: Endurance (sff)
Tow Ubukata Mardock Scramble (sff)
Sayuri Ueda The Cage of Zeus (sff)
Sean Williams & Shane Dix Echoes of Earth (sff)
Hiroshi Yamamoto MM9 (sff)
Timothy Zahn Blackcollar (sff)
Phew. Okay, all caught up, and hopefully won't have to dump something like this again in the near future. Also, more books than I have any actual time to read, but what else is new.

Antoine Beaupr : A comparison of cryptographic keycards

An earlier article showed that private key storage is an important problem to solve in any cryptographic system and established keycards as a good way to store private key material offline. But which keycard should we use? This article examines the form factor, openness, and performance of four keycards to try to help readers choose the one that will fit their needs. I have personally been using a YubiKey NEO, since a 2015 announcement on GitHub promoting two-factor authentication. I was also able to hook up my SSH authentication key into the YubiKey's 2048 bit RSA slot. It seemed natural to move the other subkeys onto the keycard, provided that performance was sufficient. The mail client that I use, (Notmuch), blocks when decrypting messages, which could be a serious problems on large email threads from encrypted mailing lists. So I built a test harness and got access to some more keycards: I bought a FST-01 from its creator, Yutaka Niibe, at the last DebConf and Nitrokey donated a Nitrokey Pro. I also bought a YubiKey 4 when I got the NEO. There are of course other keycards out there, but those are the ones I could get my hands on. You'll notice none of those keycards have a physical keypad to enter passwords, so they are all vulnerable to keyloggers that could extract the key's PIN. Keep in mind, however, that even with the PIN, an attacker could only ask the keycard to decrypt or sign material but not extract the key that is protected by the card's firmware.

Form factor The Nitrokey Pro, YubiKey NEO (worn out), YubiKey 4, and FST-01 The four keycards have similar form factors: they all connect to a standard USB port, although both YubiKey keycards have a capacitive button by which the user triggers two-factor authentication and the YubiKey 4 can also require a button press to confirm private key use. The YubiKeys feel sturdier than the other two. The NEO has withstood two years of punishment in my pockets along with the rest of my "real" keyring and there is only minimal wear on the keycard in the picture. It's also thinner so it fits well on the keyring. The FST-01 stands out from the other two with its minimal design. Out of the box, the FST-01 comes without a case, so the circuitry is exposed. This is deliberate: one of its goals is to be as transparent as possible, both in terms of software and hardware design and you definitely get that feeling at the physical level. Unfortunately, that does mean it feels more brittle than other models: I wouldn't carry it in my pocket all the time, although there is a case that may protect the key a little better, but it does not provide an easy way to hook it into a keyring. In the group picture above, the FST-01 is the pink plastic thing, which is a rubbery casing I received along with the device when I got it. Notice how the USB connectors of the YubiKeys differ from the other two: while the FST-01 and the Nitrokey have standard USB connectors, the YubiKey has only a "half-connector", which is what makes it thinner than the other two. The "Nano" form factor takes this even further and almost disappears in the USB port. Unfortunately, this arrangement means the YubiKey NEO often comes loose and falls out of the USB port, especially when connected to a laptop. On my workstation, however, it usually stays put even with my whole keyring hanging off of it. I suspect this adds more strain to the host's USB port but that's a tradeoff I've lived with without any noticeable wear so far. Finally, the NEO has this peculiar feature of supporting NFC for certain operations, as LWN previously covered, but I haven't used that feature yet. The Nitrokey Pro looks like a normal USB key, in contrast with the other two devices. It does feel a little brittle when compared with the YubiKey, although only time will tell how much of a beating it can take. It has a small ring in the case so it is possible to carry it directly on your keyring, but I would be worried the cap would come off eventually. Nitrokey devices are also two times thicker than the Yubico models which makes them less convenient to carry around on keyrings.

Open and closed designs The FST-01 is as open as hardware comes, down to the PCB design available as KiCad files in this Git repository. The software running on the card is the Gnuk firmware that implements the OpenPGP card protocol, but you can also get it with firmware implementing a true random number generator (TRNG) called NeuG (pronounced "noisy"); the device is programmable through a standard Serial Wire Debug (SWD) port. The Nitrokey Start model also runs the Gnuk firmware. However, the Nitrokey website announces only ECC and RSA 2048-bit support for the Start, while the FST-01 also supports RSA-4096. Nitrokey's founder Jan Suhr, in a private email, explained that this is because "Gnuk doesn't support RSA-3072 or larger at a reasonable speed". Its devices (the Pro, Start, and HSM models) use a similar chip to the FST-01: the STM32F103 microcontroller. Nitrokey Pro with STM32F103TBU6 MCU Nitrokey also publishes its hardware designs, on GitHub, which shows the Pro is basically a fork of the FST-01, according to the ChangeLog. I opened the case to confirm it was using the STM MCU, something I should warn you against; I broke one of the pins holding it together when opening it so now it's even more fragile. But at least, I was able to confirm it was built using the STM32F103TBU6 MCU, like the FST-01. Nitrokey back side But this is where the comparison ends: on the back side, we find a SIM card reader that holds the OpenPGP card that, in turn, holds the private key material and does the cryptographic operations. So, in effect, the Nitrokey Pro is really a evolution of the original OpenPGP card readers. Nitrokey confirmed the OpenPGP card featured in the Pro is the same as the one shipped by the Free Software Foundation Europe (FSFE): the BasicCard built by ZeitControl. Those cards, however, are covered by NDAs and the firmware is only partially open source. This makes the Nitrokey Pro less open than the FST-01, but that's an inevitable tradeoff when choosing a design based on the OpenPGP cards, which Suhr described to me as "pretty proprietary". There are other keycards out there, however, for example the SLJ52GDL150-150k smartcard suggested by Debian developer Yves-Alexis Perez, which he prefers as it is certified by French and German authorities. In that blog post, he also said he was experimenting with the GPL-licensed OpenPGP applet implemented by the French ANSSI. But the YubiKey devices are even further away in the closed-design direction. Both the hardware designs and firmware are proprietary. The YubiKey NEO, for example, cannot be upgraded at all, even though it is based on an open firmware. According to Yubico's FAQ, this is due to "best security practices": "There is a 'no upgrade' policy for our devices since nothing, including malware, can write to the firmware." I find this decision questionable in a context where security updates are often more important than trying to design a bulletproof design, which may simply be impossible. And the YubiKey NEO did suffer from critical security issue that allowed attackers to bypass the PIN protection on the card, which raises the question of the actual protection of the private key material on those cards. According to Niibe, "some OpenPGP cards store the private key unencrypted. It is a common attitude for many smartcard implementations", which was confirmed by Suhr: "the private key is protected by hardware mechanisms which prevent its extraction and misuse". He is referring to the use of tamper resistance. After that security issue, there was no other option for YubiKey NEO users than to get a new keycard (for free, thankfully) from Yubico, which also meant discarding the private key material on the key. For OpenPGP keys, this may mean having to bootstrap the web of trust from scratch if the keycard was responsible for the main certification key. But at least the NEO is running free software based on the OpenPGP card applet and the source is still available on GitHub. The YubiKey 4, on the other hand, is now closed source, which was controversial when the new model was announced last year. It led the main Linux Foundation system administrator, Konstantin Ryabitsev, to withdraw his endorsement of Yubico products. In response, Yubico argued that this approach was essential to the security of its devices, which are now based on "a secure chip, which has built-in countermeasures to mitigate a long list of attacks". In particular, it claims that:
A commercial-grade AVR or ARM controller is unfit to be used in a security product. In most cases, these controllers are easy to attack, from breaking in via a debug/JTAG/TAP port to probing memory contents. Various forms of fault injection and side-channel analysis are possible, sometimes allowing for a complete key recovery in a shockingly short period of time.
While I understand those concerns, they eventually come down to the trust you have in an organization. Not only do we have to trust Yubico, but also hardware manufacturers and designs they have chosen. Every step in the hidden supply chain is then trusted to make correct technical decisions and not introduce any backdoors. History, unfortunately, is not on Yubico's side: Snowden revealed the example of RSA security accepting what renowned cryptographer Bruce Schneier described as a "bribe" from the NSA to weaken its ECC implementation, by using the presumably backdoored Dual_EC_DRBG algorithm. What makes Yubico or its suppliers so different from RSA Security? Remember that RSA Security used to be an adamant opponent to the degradation of encryption standards, campaigning against the Clipper chip in the first crypto wars. Even if we trust the Yubico supply chain, how can we trust a closed design using what basically amounts to security through obscurity? Publicly auditable designs are an important tradition in cryptography, and that principle shouldn't stop when software is frozen into silicon. In fact, a critical vulnerability called ROCA disclosed recently affects closed "smartcards" like the YubiKey 4 and allows full private key recovery from the public key if the key was generated on a vulnerable keycard. When speaking with Ars Technica, the researchers outlined the importance of open designs and questioned the reliability of certification:
Our work highlights the dangers of keeping the design secret and the implementation closed-source, even if both are thoroughly analyzed and certified by experts. The lack of public information causes a delay in the discovery of flaws (and hinders the process of checking for them), thereby increasing the number of already deployed and affected devices at the time of detection.
This issue with open hardware designs seems to be recurring topic of conversation on the Gnuk mailing list. For example, there was a discussion in September 2017 regarding possible hardware vulnerabilities in the STM MCU that would allow extraction of encrypted key material from the key. Niibe referred to a talk presented at the WOOT 17 workshop, where Johannes Obermaier and Stefan Tatschner, from the Fraunhofer Institute, demonstrated attacks against the STMF0 family MCUs. It is still unclear if those attacks also apply to the older STMF1 design used in the FST-01, however. Furthermore, extracted private key material is still protected by user passphrase, but the Gnuk uses a weak key derivation function, so brute-forcing attacks may be possible. Fortunately, there is work in progress to make GnuPG hash the passphrase before sending it to the keycard, which should make such attacks harder if not completely pointless. When asked about the Yubico claims in a private email, Niibe did recognize that "it is true that there are more weak points in general purpose implementations than special implementations". During the last DebConf in Montreal, Niibe explained:
If you don't trust me, you should not buy from me. Source code availability is only a single factor: someone can maliciously replace the firmware to enable advanced attacks.
Niibe recommends to "build the firmware yourself", also saying the design of the FST-01 uses normal hardware that "everyone can replicate". Those advantages are hard to deny for a cryptographic system: using more generic components makes it harder for hostile parties to mount targeted attacks. A counter-argument here is that it can be difficult for a regular user to audit such designs, let alone physically build the device from scratch but, in a mailing list discussion, Debian developer Ian Jackson explained that:
You don't need to be able to validate it personally. The thing spooks most hate is discovery. Backdooring supposedly-free hardware is harder (more costly) because it comes with greater risk of discovery. To put it concretely: if they backdoor all of them, someone (not necessarily you) might notice. (Backdooring only yours involves messing with the shipping arrangements and so on, and supposes that you specifically are of interest.)
Since that, as far as we know, the STM microcontrollers are not backdoored, I would tend to favor those devices instead of proprietary ones, as such a backdoor would be more easily detectable than in a closed design. Even though physical attacks may be possible against those microcontrollers, in the end, if an attacker has physical access to a keycard, I consider the key compromised, even if it has the best chip on the market. In our email exchange, Niibe argued that "when a token is lost, it is better to revoke keys, even if the token is considered secure enough". So like any other device, physical compromise of tokens may mean compromise of the key and should trigger key-revocation procedures.

Algorithms and performance To establish reliable performance results, I wrote a benchmark program naively called crypto-bench that could produce comparable results between the different keys. The program takes each algorithm/keycard combination and runs 1000 decryptions of a 16-byte file (one AES-128 block) using GnuPG, after priming it to get the password cached. I assume the overhead of GnuPG calls to be negligible, as it should be the same across all tokens, so comparisons are possible. AES encryption is constant across all tests as it is always performed on the host and fast enough to be irrelevant in the tests. I used the following:
  • Intel(R) Core(TM) i3-6100U CPU @ 2.30GHz running Debian 9 ("stretch"/stable amd64), using GnuPG 2.1.18-6 (from the stable Debian package)
  • Nitrokey Pro 0.8 (latest firmware)
  • FST-01, running Gnuk version 1.2.5 (latest firmware)
  • YubiKey NEO OpenPGP applet 1.0.10 (not upgradable)
  • YubiKey 4 4.2.6 (not upgradable)
I ran crypto-bench for each keycard, which resulted in the following:
Algorithm Device Mean time (s)
ECDH-Curve25519 CPU 0.036
FST-01 0.135
RSA-2048 CPU 0.016
YubiKey-4 0.162
Nitrokey-Pro 0.610
YubiKey-NEO 0.736
FST-01 1.265
RSA-4096 CPU 0.043
YubiKey-4 0.875
Nitrokey-Pro 3.150
FST-01 8.218
Decryption graph There we see the performance of the four keycards I tested, compared with the same operations done without a keycard: the "CPU" device. That provides the baseline time of GnuPG decrypting the file. The first obvious observation is that using a keycard is slower: in the best scenario (FST-01 + ECC) we see a four-fold slowdown, but in the worst case (also FST-01, but RSA-4096), we see a catastrophic 200-fold slowdown. When I presented the results on the Gnuk mailing list, GnuPG developer Werner Koch confirmed those "numbers are as expected":
With a crypto chip RSA is much faster. By design the Gnuk can't be as fast - it is just a simple MCU. However, using Curve25519 Gnuk is really fast.
And yes, the FST-01 is really fast at doing ECC, but it's also the only keycard that handles ECC in my tests; the Nitrokey Start and Nitrokey HSM should support it as well, but I haven't been able to test those devices. Also note that the YubiKey NEO doesn't support RSA-4096 at all, so we can only compare RSA-2048 across keycards. We should note, however, that ECC is slower than RSA on the CPU, which suggests the Gnuk ECC implementation used by the FST-01 is exceptionally fast. In discussions about improving the performance of the FST-01, Niibe estimated the user tolerance threshold to be "2 seconds decryption time". In a new design using the STM32L432 microcontroller, Aurelien Jarno was able to bring the numbers for RSA-2048 decryption from 1.27s down to 0.65s, and for RSA-4096, from 8.22s down to 3.87s seconds. RSA-4096 is still beyond the two-second threshold, but at least it brings the FST-01 close to the YubiKey NEO and Nitrokey Pro performance levels. We should also underline the superior performance of the YubiKey 4: whatever that thing is doing, it's doing it faster than anyone else. It does RSA-4096 faster than the FST-01 does RSA-2048, and almost as fast as the Nitrokey Pro does RSA-2048. We should also note that the Nitrokey Pro also fails to cross the two-second threshold for RSA-4096 decryption. For me, the FST-01's stellar performance with ECC outshines the other devices. Maybe it says more about the efficiency of the algorithm than the FST-01 or Gnuk's design, but it's definitely an interesting avenue for people who want to deploy those modern algorithms. So, in terms of performance, it is clear that both the YubiKey 4 and the FST-01 take the prize in their own areas (RSA and ECC, respectively).

Conclusion In the above presentation, I have evaluated four cryptographic keycards for use with various OpenPGP operations. What the results show is that the only efficient way of storing a 4096-bit encryption key on a keycard would be to use the YubiKey 4. Unfortunately, I do not feel we should put our trust in such closed designs so I would argue you should either stick with 2048-bit encryption subkeys or keep the keys on disk. Considering that losing such a key would be catastrophic, this might be a good approach anyway. You should also consider switching to ECC encryption: even though it may not be supported everywhere, GnuPG supports having multiple encryption subkeys on a keyring: if one algorithm is unsupported (e.g. GnuPG 1.4 doesn't support ECC), it will fall back to a supported algorithm (e.g. RSA). Do not forget your previously encrypted material doesn't magically re-encrypt itself using your new encryption subkey, however. For authentication and signing keys, speed is not such an issue, so I would warmly recommend either the Nitrokey Pro or Start, or the FST-01, depending on whether you want to start experimenting with ECC algorithms. Availability also seems to be an issue for the FST-01. While you can generally get the device when you meet Niibe in person for a few bucks (I bought mine for around \$30 Canadian), the Seeed online shop says the device is out of stock at the time of this writing, even though Jonathan McDowell said that may be inaccurate in a debian-project discussion. Nevertheless, this issue may make the Nitrokey devices more attractive. When deciding on using the Pro or Start, Suhr offered the following advice:
In practice smart card security has been proven to work well (at least if you use a decent smart card). Therefore the Nitrokey Pro should be used for high security cases. If you don't trust the smart card or if Nitrokey Start is just sufficient for you, you can choose that one. This is why we offer both models.
So far, I have created a signing subkey and moved that and my authentication key to the YubiKey NEO, because it's a device I physically trust to keep itself together in my pockets and I was already using it. It has served me well so far, especially with its extra features like U2F and HOTP support, which I use frequently. Those features are also available on the Nitrokey Pro, so that may be an alternative if I lose the YubiKey. I will probably move my main certification key to the FST-01 and a LUKS-encrypted USB disk, to keep that certification key offline but backed up on two different devices. As for the encryption key, I'll wait for keycard performance to improve, or simply switch my whole keyring to ECC and use the FST-01 or Nitrokey Start for that purpose.
[The author would like to thank Nitrokey for providing hardware for testing.] This article first appeared in the Linux Weekly News.

2 October 2017

James McCoy: Monthly FLOSS activity - 2017/09 edition

Debian devscripts Before deciding to take an indefinite hiatus from devscripts, I prepared one more upload merging various contributed patches and a bit of last minute cleanup. I also setup integration with Travis CI to hopefully catch issues sooner than "while preparing an upload", as was typically the case before. Anyone with push access to the Debian/devscripts GitHub repo can take advantage of this to test out changes, or keep the development branches up to date. In the process, I was able to make some improvements to travis.debian.net, namely support for DEB_BUILD_PROFILES and using a separate, minimal docker image for running autopkgtests. unibilium neovim Oddly, the mips64el builds were in BD-Uninstallable state, even though luajit's buildd status showed it was built. Looking further, I noticed the libluajit-5.1 ,-dev binary packages didn't have the mips64el architecture enabled, so I asked for it to be enabled. msgpack-c There were a few packages left which would FTBFS if I uploaded msgpack-c 2.x to unstable. All of the bug reports had either trivial work arounds (i.e., forcing use of the v1 C++ API) or trivial patches. However, I didn't want to continue waiting for the packages to get fixed since I knew other people had expressed interest in the new msgpack-c. Trying to avoid making other packages insta-buggy, I NMUed autobahn-cpp with the v1 work around. That didn't go over well, partly because I didn't send a finalized "Hey, I'd like to get this done and here's my plan to NMU" email. Based on that feedback, I decided to bump the remaining bugs to "serious" instead of NMUing and upload msgpack-c. Thanks to Jonas Smedegaard for quickly integrating my proposed fix for libdata-messagepack-perl. Hopefully, upstream has some time to review the PR soon. vim subversion
neovim

21 September 2017

Clint Adams: PTT

Hello, said Adrian, but Adrian was lying. My name is Adrian, said Adrian, but Adrian was lying. Today I took a pic of myself pulling a train, announced Adrian. Spaniard pulling a train
Posted on 2017-09-21
Tags: bgs

2 September 2017

Clint Adams: Litigants

Bronwyn s mom got hit by a semi. She was on the passenger side of the car, the side of impact, and she did not rebound with extreme resilience. The family sued the trucking company and came away with a settlement of roughly $10 million. The lawyers took $6.5 million of that: quite a deal. Bronwyn learned two things from this, and neither one was about Christopher Lloyd.
Posted on 2017-09-02
Tags: mintings

1 September 2017

Clint Adams: Good night moon and spoon balloon

Hello, said Adrian, but Adrian was lying. My name is Adrian, said Adrian, but Adrian was lying.
Posted on 2017-09-01
Tags: bgs

29 August 2017

Dirk Eddelbuettel: RcppSMC 0.2.0

A new version 0.2.0 of the RcppSMC package arrived on CRAN earlier today (as a very quick pretest-publish within minutes of submission). RcppSMC provides Rcpp-based bindings to R for the Sequential Monte Carlo Template Classes (SMCTC) by Adam Johansen described in his JSS article. This release 0.2.0 is chiefly the work of Leah South, a Ph.D. student at Queensland University of Technology, who was during the last few months a Google Summer of Code student mentored by Adam and myself. It was pleasure to work with Leah on this, and see her progress. Our congratulations to Leah for a job well done!

Changes in RcppSMC version 0.2.0 (2017-08-28)
  • Also use .registration=TRUE in useDynLib in NAMESPACE
  • Multiple Sequential Monte Carlo extensions (Leah South as part of Google Summer of Code 2017)
    • Switching to population level objects (#2 and #3).
    • Using Rcpp attributes (#2).
    • Using automatic RNGscope (#4 and #5).
    • Adding multiple normalising constant estimators (#7).
    • Static Bayesian model example: linear regression (#10 addressing #9).
    • Adding a PMMH example (#13 addressing #11).
    • Framework for additional algorithm parameters and adaptation (#19 addressing #16; also #24 addressing #23).
    • Common adaptation methods for static Bayesian models (#20 addressing #17).
    • Supporting MCMC repeated runs (#21).
    • Adding adaptation to linear regression example (#22 addressing #18).

Courtesy of CRANberries, there is a diffstat report for this release. More information is on the RcppSMC page. Issues and bugreports should go to the GitHub issue tracker.

This post by Dirk Eddelbuettel originated on his Thinking inside the box blog. Please report excessive re-aggregation in third-party for-profit settings.

27 July 2017

Joachim Breitner: Coinduction in Coq and Isabelle

The DeepSpec Summer School is almost over, and I have had a few good discussions. One revolved around coinduction: What is it, how does it differ from induction, and how do you actually prove something. In the course of the discussion, I came up with a very simple coinductive exercise, and solved it both in Coq and Isabelle

The task Define the extended natural numbers coinductively. Define the min function and the relation. Show that min(n, m) n holds.

Coq The definitions are straight forward. Note that in Coq, we use the same command to define a coinductive data type and a coinductively defined relation: 
CoInductive ENat :=
    N : ENat
    S : ENat -> ENat.
CoFixpoint min (n : ENat) (m : ENat)
  :=match n, m with   S n', S m' => S (min n' m')
                      _, _       => N end.
CoInductive le : ENat -> ENat -> Prop :=
    leN : forall m, le N m
    leS : forall n m, le n m -> le (S n) (S m).
The lemma is specified as 
Lemma min_le: forall n m, le (min n m) n.
and the proof method of choice to show that some coinductive relation holds, is cofix. One would wish that the following proof would work: 
Lemma min_le: forall n m, le (min n m) n.
Proof.
  cofix.
  destruct n, m.
  * apply leN.
  * apply leN.
  * apply leN.
  * apply leS.
    apply min_le.
Qed.
but we get the error message 
Error:
In environment
min_le : forall n m : ENat, le (min n m) n
Unable to unify "le N ?M170" with "le (min N N) N
Effectively, as Coq is trying to figure out whether our proof is correct, i.e. type-checks, it stumbled on the equation min N N = N, and like a kid scared of coinduction, it did not dare to run the min function. The reason it does not just run a CoFixpoint is that doing so too daringly might simply not terminate. So, as Adam explains in a chapter of his book, Coq reduces a cofixpoint only when it is the scrutinee of a match statement. So we need to get a match statement in place. We can do so with a helper function: 
Definition evalN (n : ENat) :=
  match n with   N => N
                 S n => S n end.
Lemma evalN_eq : forall n, evalN n = n.
Proof. intros. destruct n; reflexivity. Qed.
This function does not really do anything besides nudging Coq to actually evaluate its argument to a constructor (N or S _). We can use it in the proof to guide Coq, and the following goes through: 
Lemma min_le: forall n m, le (min n m) n.
Proof.
  cofix.
  destruct n, m; rewrite <- evalN_eq with (n := min _ _).
  * apply leN.
  * apply leN.
  * apply leN.
  * apply leS.
    apply min_le.
Qed.

Isabelle In Isabelle, definitions and types are very different things, so we use different commands to define ENat and le: 
theory ENat imports  Main begin
codatatype ENat =  N   S  ENat
primcorec min where
   "min n m = (case n of
       N   N
       S n'   (case m of
        N   N
        S m'   S (min n' m')))"
coinductive le where
  leN: "le N m"
  leS: "le n m   le (S n) (S m)"
There are actually many ways of defining min; I chose the one most similar to the one above. For more details, see the corec tutorial. Now to the proof: 
lemma min_le: "le (min n m) n"
proof (coinduction arbitrary: n m)
  case le
  show ?case
  proof(cases n)
    case N then show ?thesis by simp
  next
    case (S n') then show ?thesis
    proof(cases m)
      case N then show ?thesis by simp
    next
      case (S m')  with  n = _  show ?thesis
        unfolding min.code[where n = n and m = m]
        by auto
    qed
  qed
qed
The coinduction proof methods produces this goal: 
proof (state)
goal (1 subgoal):
 1.  n m. ( m'. min n m = N   n = m')  
          ( n' m'.
               min n m = S n'  
               n = S m'  
	       (( n m. n' = min n m   m' = n)   le n' m'))
I chose to spell the proof out in the Isar proof language, where the outermost proof structure is done relatively explicity, and I proceed by case analysis mimiking the min function definition. In the cases where one argument of min is N, Isabelle s simplifier (a term rewriting tactic, so to say), can solve the goal automatically. This is because the primcorec command produces a bunch of lemmas, one of which states n = N m = N min n m = N. In the other case, we need to help Isabelle a bit to reduce the call to min (S n) (S m) using the unfolding methods, where min.code contains exactly the equation that we used to specify min. Using just unfolding min.code would send this method into a loop, so we restrict it to the concrete arguments n and m. Then auto can solve the remaining goal (despite all the existential quantifiers).

Summary Both theorem provers are able to prove the desired result. To me it seems that it is slightly more convenient in Isabelle because a lot of Coq infrastructure relies on the type checker being able to effectively evaluate expressions, which is tricky with cofixpoints, wheras evaluation plays a much less central role in Isabelle, where rewriting is the crucial technique, and while one still cannot simply throw min.code into the simpset, so working with objects that do not evaluate easily or completely is less strange.

Agda I was challenged to do it in Agda. Here it is: 
module ENat where
open import Coinduction
data ENat : Set where
  N : ENat
  S :   ENat   ENat
min : ENat   ENat   ENat
min (S n') (S m') = S (  (min (  n') (  m')))
min _ _ = N
data le : ENat   ENat   Set where
  leN :    m    le N m
  leS :    n m      (le (  n) (  m))   le (S n) (S m)
min_le :    n m    le (min n m) n
min_le  S n'   S m'  = leS (  min_le)
min_le  N      S m'  = leN
min_le  S n'   N  = leN
min_le  N      N  = leN
I will refrain from commenting it, because I do not really know what I have been doing here, but it typechecks, and refer you to the official documentation on coinduction in Agda. But let me note that I wrote this using plain inductive types and recursion, and added , and until it worked.

5 June 2017

Clint Adams: nibus daisens

What s up with narcissists and sexual predators frequently reapplying their lipstick?
Posted on 2017-06-05
Tags: ranticore

29 May 2017

Clint Adams: Dots and dashes

The Canadians were on LSD. The sex-toy bag was full of booze and Olivia lost her buttplug and we had to search the kitchen drawers before she juiced the grapefruits.
Posted on 2017-05-29
Tags: mintings

19 May 2017

Clint Adams: Help the Aged

I keep meeting girls from Walnut Creek who don t know about the CDROM.
Posted on 2017-05-19
Tags: ranticore

9 May 2017

Clint Adams: Four years

#706067
Posted on 2017-05-09
Tags: barks

Next.

Previous.